
In our approach, initially  the user chooses a view $V$ and the number of rows of the initial \emph{symbolic database} instance (that is the number of rows of the tables involved in the computation of $V$).
  Each attribute value in each row
  corresponds to a fresh logic variable with its associated domain integrity constraints.
      The tool tries to obtain a positive test-case by binding the logic variables in the symbolic database. Notice that the number of rows directly affects the result since for some queries does not exists positive test-cases with an specific size.  In the future we plan to decide automatically the more convenient size by inspecting the relations definition. Observe also that currently only integer domains are supported. Extending the proposal to other domains such as strings does not seem difficult to achieve, but is beyond the scope of this work.

For instance, in Example \ref{ex:running}, suppose that the user decides to look for a positive test-case with two rows in each table. Then, initially the prototype builds the symbolic instance shown in Table \ref{inst}.
\begin{table}[ht]
\centering
\subfloat[Symbolic table player][Player]{\begin{tabular}{|c|}
\hline
\textbf{player} \\
\hline
id \\
\hline
player.id.0 \\
player.id.1 \\
\hline
\end{tabular}}
\qquad
\subfloat[Symbolic table board][Board]{\begin{tabular}{|c|c|c|}
\hline
\multicolumn{3}{|c|}{\textbf{board}} \\
\hline
id & x & y \\
\hline
board.id.0 & board.x.0 &  board.y.0 \\
board.id.1 & board.x.1 &  board.y.1 \\
\hline
\end{tabular}}
\caption{Symbolic database instance}\label{inst}
\end{table}
Notice that \cod{player.id.0, player.id.1}, \cod{board.id.0, board.id.1}, \cod{board.x.0, board.x.1}, \cod{board.y.0, board.y.1} represent logic variables.
The \hyperref[def:constraints]{next definition} is employed by the tool to establish the constraints on these variables.

\begin{definition} \label{def:constraints}
Let $D$ be a database schema and $d$ a  database instance. We define
$\theta(R,d)$ for every relation $R$ in $D$ as a multiset of pairs $(\psi,u)$ with
$\psi$ a first order formula, and $u$ a row. This multiset is defined as follows:
\begin{enumerate}
\item \label{def:constraints:table} For every table $T$ in $D$ such that $d(T)=\multi{\mu_1,\dots,\mu_n}$:
where $\mu_i$ = $(T.C_1 \mapsto X_{i1},\dots,T.C_m \mapsto X_{im})$ then:
\begin{itemize}
\item  If the definition of $T$ has neither primary key nor foreign key constraints:
  $\theta(T,d) = \multi{ (true,\mu_1), \dots, (true,\mu_n) }$.
\item If the definition of $T$ contains primary or foreign key constraints:
\begin{itemize}
\item \label{def:constraints:primary} if $T$ has a primary key constraint for the columns $C_1, \dots, C_p $:
  Let $T'$ be the table $T$ without that primary key constraint.
  Assume that $\theta(T',d) = \multileft (\psi_1,\mu_1),$ $\dots,$ $(\psi_n,\mu_n) \multiright$, then:
$$\theta(T,d) = \multi{((\psi_i \wedge (\bigwedge_{j=1, j\neq i}^n(\bigvee_{k=1}^p \mu_i(T.C_k) \neq \mu_j(T.C_k) ))),\mu_i)|i \in 1,\dots,n}$$

\item \label{def:constraints:foreign} if $T$ has a foreign key constraint for the columns $T.C_1, \dots, T.C_f $ referring the columns $T2.C'_1,...T2.C'_f$ from table $T2$:
  Let $T'$ be the $T$ without that foreign key constraint.
  Assume that $\theta(T',d) = \multi{ (\psi_1,\mu_1), \dots, (\psi_n,\mu_n) }$, and that  $d(T_2) = \multi{\nu_1, \dots, \nu_{n'}}$. Then:
$$\theta(T,d) = \multi{((\psi_i \wedge (\bigvee_{j=1, j\neq i}^{n'}(\bigwedge_{k=1}^f \mu_i(T.C_k) = \nu_j(T2.C'_k) ))),\mu_i)|i \in 1,\dots,n}$$
\end{itemize}
\end{itemize}
\item \label{def:constraints:view} For every view $V =$ {\sf create view} V($E_1$, \dots, $E_n$) {\sf as} $Q$,
     $$\theta(V,d) = \theta(Q,d)\{V.E_1 \mapsto Q.A_1, \dots, V.E_n\mapsto A_n   \}$$


\item \label{def:constraints:basic} If $Q$ is a basic query of the form:
$$
\begin{array}{rl}
  &\textrm{\sf select }e_1, \dots, e_n \  {\sf from }\ R_1\ B_1 , \dots, R_m \ B_m\  \textrm{\sf where}\ C_w;
\end{array}
$$
Then:
$$
   \begin{array}{ll}
  \theta(Q,d) = & \multileft{ (\psi_1 \wedge \dots \wedge \psi_m \wedge \ftx{C_w\mu}{d},\,s_Q(\mu))\ \mid } \\
              &\quad   (\psi_1, \nu_1) \in \theta(R_1,d), \dots, (\psi_m, \nu_m) \in \theta(R_m,d),  \mu = {\nu_1}^{B_1} \odot \cdots \odot {\nu_m}^{B_m}   \multiright
  \end{array}
$$
  where
  \begin{itemize}
   \item $s_Q(\mu)$ = $\{Q.A_1 \mapsto (e_1 \mu), \dots, Q.A_n \mapsto (e_n \mu) \}$,
   \item The first order formula $\ftx{C}{d}$ is defined as
   \begin{itemize}
        \item If $C \equiv \cod{false}$ then  $\ftx{C}{d} = \bot$
        \item If $C \equiv \cod{true}$ then  $\ftx{C}{d} = \top$
        \item If $C \equiv e$, with $e$ an arithmetic expression involving constants then
              $\ftx{C}{d} = e$
        \item If $C \equiv e_1 \diamond e_2$, with  $\diamond$ a relational operator, then  $\ftx{C}{d} = (\ftx{e_1}{d} \diamond \ftx{e_2}{d})$ .
        \item If $C \equiv C_1\ \cod{ and }\ C_2$ then $\ftx{C}{d} = \ftx{C_1}{d} \wedge \ftx{C_2}{d}$
        \item If $C \equiv C_1\ \cod{ or }\ C_2$ then $\ftx{C}{d} =\ftx{C_1}{d} \vee \ftx{C_2}{d}$
        \item If $C \equiv \cod{ not }\ C_1$ then $\ftx{C}{d} = \neg \ftx{C}{d}$
        \item If $C \equiv \cod{ exists }\ Q$ then
        suppose that
         $\theta(Q,d) = \multi{ (\psi_1, \mu_1), \dots (\psi_{p},\mu_{p}) }$.
     Then  $\ftx{C}{d} = (\vee_{j=1}^{p} \psi_j)$.

        \end{itemize}

 \end{itemize}
\item \label{def:constraints:set} For set queries:
     \begin{itemize}
    \item  $ \theta(V_1 \ \textrm{\sf union }\ V_2,d) = \theta({V_1},d)\ \cup\ \theta({V_2},d)$
                with $\cup$ the multiset union.
    \item $(\psi,\mu) \in \theta(V_1\ \textrm{\sf intersection }\ V_2,d)$   with cardinality  $k$ iff
          $(\psi_1,\mu) \in \theta(V_1,d)$ with cardinality $k_1$, $(\psi_2,\mu) \in \theta(V_2,d)$
          with cardinality $k_2$, $k=min(k_1,k_2)$ and $\psi = \psi_1 \wedge \psi_2$.
    \end{itemize}


\end{enumerate}
\end{definition}

Observe that the notation $s_Q(x)$  with $Q$ a query is a shorthand for the row $\mu$ with
domain $\{E_1, \dots, E_n \}$ such that $(E_i)x = (e_i)x$, with $i=1 \dots n$,
with {\sf select $e_1$ $E_1$, \dots, $e_n$ $E_n$}  the {\sf select} clause of $Q$.
If $E_i$'s are omitted in the query, it is assumed that $E_i = e_i$.



The following result and its corollary represent the main result of this paper, stating the
soundness and completeness of our proposal:

\begin{theorem} \label{theo}
Let $D$ be a database schema and $d$ a valid database instance. Let $R$ be either a relation in $D$ or a query defined using relations in $D$.
Then $\eta \in \SQL{R,d}$ with cardinality $k$  iff $(true,\eta) \in \theta(R,d)$ with cardinality $k$.

\end{theorem}

\begin{proof}
\input{demo}
\end{proof}

Observe that in \cite{flops2010} the proof was restricted to queries without subqueries due to the limitations of
the Extended Relational Algebra \cite{Molina08} used as operational semantics.

%However we have decided to keep this feature in our setting because subqueries are very common
%in practical queries and usually they are not considered in the literature.
The following corollary contains the idea for generating  constraints  that
will yield the PTCs:


\begin{corollary} \label{coro}
Let $D$ be a database schema and $d_s$ a symbolic database instance.
Let $R$ be a relation in $D$
such that $\theta(R) = \multi{ (\psi_1, \mu_1), \dots (\psi_n,\mu_n) }$,
and $\eta$ a substitution satisfying  $d_s$.
Then $d_s\eta$ is a PTC for $R$ iff
$(\bigvee_{i=1}^n \psi_i)\eta = true$.
\end{corollary}
\begin{proof}
Straightforward from Theorem \ref{theo}:  $(\bigvee_{i=1}^n \psi_i)\eta = true$ iff
there is some $\psi_i$ with $1 \leq i \leq n$ such that $\psi_i\eta = true$ iff
 $(\mu_i\eta) \in \SQL{R}$ iff  $\SQL{R} \neq \emptyset$.
\end{proof}

